In formal verification, a tool needs to solve a set of properties, such as System Verilog assertions (SVAs). These properties are either automatically generated by the tool, manually specified by the tool user, or provided in some other way.
Given a fixed computational resource budget (CPU time, memory, number of available machines), the formal tool's performance is measured by the number of properties solved within the resource budget. Properties not solved at the end of the execution will have a timed out status.
To maximize the tool's throughput, it is advantageous to schedule the properties such that easier properties are solved first. However, it is a very challenging problem to estimate the hardness of properties without actually solving the problem.
One prior art method of estimating is calculating the theoretical upper bound of formal property, which gives an estimate of the hardness of the property. If there are m variables in the cone of influence (COI) logic of the properties, the upper bound estimates the CPU time to solve the property is in O(2{circumflex over ( )}m) using big-O notation. In a standard test case, a typical property can 50,000 variables or more. The value of O(2{circumflex over ( )}50000) is a huge number. However, modern formal tools can often solve many properties within minutes or hours. This shows that the theoretical upper bound is too rough to be useful in practice, and does not correlate well to the empirical hardness.
Another prior art method of estimating empirical hardness uses ad-hoc heuristics. They are typically in the form of handcrafted formula based on a few feature variables, e.g., the number of input variables, the number of sequential state variables in the COI of the property. In these approaches, the empirical hardness of the property is modeled by some linear or non-linear functions, often done by a domain expert. Parameters in these functions are then fitted to the given data set using regression technique. Essentially, these approaches use linear regression techniques to approximate the empirical hardness of a property.
There are at least two major drawbacks with these ad-hoc heuristics. The first drawback is caused by “the limited feature set”. These formulas are hand-crafted by a domain expert and typically only involve just a small number (<10) of feature variables, since formal properties with large number variables are very difficult for a human being to comprehend. The second drawback is caused by “the absolute objective function”. These approaches try to estimate the empirical hardness of a property directly, i.e., they try to predict the actual CPU time required to solve a property. This is a highly non-linear objective function and hard to model with standard regression techniques. In practice, these heuristics often give low prediction accuracy on unseen examples and are not used in a formal product.